\begin{tabbing}
$\forall$$T$:Type, $L_{1}$, $L_{2}$, $L$:$T$ List.
\\[0ex]disjoint\_sublists($T$;$L_{1}$;$L_{2}$;$L$)
\\[0ex]$\Rightarrow$ (\=$\exists$$f$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$+$\parallel$$L_{2}$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$).\+
\\[0ex]Inj($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$+$\parallel$$L_{2}$$\parallel$}}$; $\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$; $f$)
\\[0ex]\& (\=$\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$+$\parallel$$L_{2}$$\parallel$}}$.\+
\\[0ex]($i$$<\parallel$$L_{1}$$\parallel$ $\Rightarrow$ $L_{1}$[$i$] $=$ $L$[$f$($i$)] $\in$ $T$) \& ($\parallel$$L_{1}$$\parallel\leq$$i$ $\Rightarrow$ $L_{2}$[$i$$-\parallel$$L_{1}$$\parallel$] $=$ $L$[$f$($i$)] $\in$ $T$)))
\-\-
\end{tabbing}